Skip to content

Include SSA lhs and rhs in extended JSON trace #4914

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Include SSA lhs and rhs in extended JSON trace #4914

wants to merge 1 commit into from

Conversation

tautschnig
Copy link
Collaborator

The full SSA identifiers will permit building tools that trace
assigned values back to inputs.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov-io
Copy link

codecov-io commented Jul 17, 2019 •
edited by codecov bot
Loading

Codecov Report

Merging #4914 (7a4135f) into develop (602e2e8) will decrease coverage by 0.04%.
The diff coverage is 100.00%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #4914      +/-   ##
===========================================
- Coverage    69.24%   69.19%   -0.05%     
===========================================
  Files         1309     1307       -2     
  Lines       108476   107967     -509     
===========================================
- Hits         75117    74712     -405     
+ Misses       33359    33255     -104
Impacted Files Coverage Δ
src/goto-programs/goto_trace.h 100.00% <100.00%> (ø)
src/goto-programs/json_goto_trace.cpp 82.78% <100.00%> (+1.20%) ⬆️
src/goto-symex/build_goto_trace.cpp 87.67% <100.00%> (+0.17%) ⬆️
src/statement-list/statement_list_typecheck.cpp 65.09% <0.00%> (-8.30%) ⬇️
src/statement-list/statement_list_entry_point.cpp 84.12% <0.00%> (-3.76%) ⬇️
...olvers/strings/string_constraint_instantiation.cpp 90.10% <0.00%> (-3.30%) ⬇️
src/util/format_expr.cpp 72.18% <0.00%> (-3.01%) ⬇️
src/goto-symex/renaming_level.cpp 92.53% <0.00%> (-2.52%) ⬇️
src/util/json.cpp 83.67% <0.00%> (-2.27%) ⬇️
src/statement-list/parser.y 89.70% <0.00%> (-1.44%) ⬇️
... and 102 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 602e2e8...617ef0d. Read the comment docs.

allredj
allredj reviewed Jul 17, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 7a4135f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/119404690

smowton
smowton reviewed Jul 17, 2019
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's have a couple of regression tests exercising this, then lgtm

@tautschnig
Copy link
Collaborator Author

Let's have a couple of regression tests exercising this, then lgtm

Which aspects specifically would you like to see tested? Right now, there is one test checking "yes, something is printed." Since the consumer is not yet very well-defined (tentatively cbmc-viewer) I'm not entirely sure what the expectation is.

@smowton
Copy link
Contributor

smowton commented Jul 17, 2019

Given the support you've added, I'd expect a program with only a declaration in addition to the assignment already tested; other than that as you say the requirements are pretty weak so far

allredj
allredj reviewed Jul 17, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 754b245).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/119481318

@kroening
Copy link
Member

Note that we used to have these fields.

Part of the rationale for removing them was the idea that a "goto trace" should be an artefact that is just that -- and independent of how it got computed. In particular, a goal was that it should be possible to produce one using a simulator or plain execution.

I am wondering whether the higher-level goal (dependency analysis) can perhaps be achieved in other ways?

@tautschnig tautschnig self-assigned this Aug 5, 2019
@tautschnig
Copy link
Collaborator Author

I am wondering whether the higher-level goal (dependency analysis) can perhaps be achieved in other ways?

@kroening All ideas welcome - it's about ways to understand how we arrived at a certain value being assigned. With CBMC's scalability improving, counterexamples get longer and thus become less useful as a diagnostic tool. This is just what seemed like the simplest step.

@tautschnig
Include SSA lhs and rhs in extended JSON trace
617ef0d 
The full SSA identifiers will permit building tools that trace
assigned values back to inputs.
@tautschnig
Copy link
Collaborator Author

Follow-up note: maybe --localize-fault is the way to go, but then it needs to be made to work. At present, its regression tests are the only cases where I am not getting "unable to localize fault."

@martin-cs
Copy link
Collaborator

All ideas... well... we could implement an ai_history_baset child that uses the goto_trace to control the abstract interpreter and use it's dependency and information flow tracking.

@tautschnig tautschnig mentioned this pull request Nov 25, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@smowton smowton smowton left review comments

@allredj allredj allredj left review comments

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

At least 1 approving review is required to merge this pull request.

Assignees

@tautschnig tautschnig

@kroening kroening

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@tautschnig @codecov-io @smowton @kroening @martin-cs @allredj